<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
  <head>
    <title>package alloy.bool</title>
  </head>

  <body>
    <p>Classes for constructing Boolean DAGs, and for interacting
    with satisfiability solvers.</p>

    <h2>Boolean DAGs</h2>

    <p>Here we will describe the generalized Boolean DAG structure used by Alloy Analyzer.
      The DAG represents a predicate on a group of Boolean variables.  It has the usual
      Boolean DAG nodes ({@linkplain alloy.bool.GBF_Const constant}, {@linkplain alloy.bool.GBF_Lit literal},
      {@linkplain alloy.bool.GBF_And AND}, {@linkplain alloy.bool.GBF_Or OR}, {@linkplain alloy.bool.GBF_Not NOT}) but also some special nodes
      ({@link alloy.bool.CNFFunc}, {@link alloy.bool.SetVarExpr}, {@link alloy.bool.VarConst}).  Still, the function of the overall DAG
      remains to express a predicate on a group of Boolean variables.  Despite the presence of nonstandard
      Boolean nodes, we will usually refer to the structure simply as "Boolean DAG".</p>

    <p>
      Boolean formula nodes of the Boolean DAG, Boolean formulas and (Boolean) expressions are all interchangeable terms,
      used in this package to refer to Boolean DAG nodes.
      </p>

    <h2>Non-standard Boolean nodes used in our Boolean DAG</h2>
    <h3>{@link alloy.bool.CNFFunc}</h3>
    <p>The {@link alloy.bool.CNFFunc} node computes an arbitrary Boolean function of its children; the AND/OR/NOT nodes
      could be implemented as CNFFunc nodes.  The arbitrary Boolean function is specified declaratively by a set of
      CNF clauses.  The function could even be non-deterministic.
      </p>

    <h3>Switch setters and switchable constants</h3>

    <p>
      {@linkplain alloy.bool.SetVarExpr Switch setters} and
      {@linkplain alloy.bool.VarConst switchable constants} are used
      to compactly encode translations of quantified Alloy formulas.
      The semantics of these nodes is as follows.  A switch setter has
      a reference to a {@linkplain alloy.bool.BoolSwitch switch}, and
      an integer value to be assigned to the switch.  It also has one
      child node, an arbitrary BooleanFormula.  The meaning of a
      switch node is that the switch is set to the integer value, and
      then the meaning of the child node is taken.  The meaning of the
      child node may depend on the value of the switch, if the sub-DAG
      rooted at the child node contains {@linkplain
      alloy.bool.VarConst switchable constants}.  A switchable
      constant is a leaf Boolean DAG node associated with a particular
      bit of a particular switch.  The meaning of a switchable
      constant is either constant true or constant false, depending on
      the current value of the bit of the switch that the switchable
      constant depends on.  The value of the switch depends on the
      last switch setter node for this switch that we have traversed
      while traversing the Boolean DAG.  So, to know the meaning of a
      Boolean DAG (i.e. the ordinary Boolean DAG it corresponds to)
      you need an assignment of values to all the free switches
      referenced in the Boolean DAG.</p>
    

    <h3>Lifted vs ground DAGs</h3>
    <p>
      A ground DAG is one that does not contain the special nodes {@link alloy.bool.SetVarExpr} (switch setters) and
      {@link alloy.bool.VarConst} (switchable constants); a lifted DAG is one that does.  
      </p>

    <p>The role of Boolean DAGs in the workflow of the Alloy Analyzer is as follows.  From a
      translatable AST we {@linkplain alloy.transl.TranslVisitor construct}
      a lifted Boolean DAG, {@linkplain alloy.bool.WriteSAT_V write} it to a .sat file, then call the SatLab
      program "sat2cnf" (see alloy2/SatLab/src/sat2cnf) to 
      </p>

    <p>The code for grounding-out is currently implemented in SatLab; there is no grounding-out code in Java.</p>

    <h3>Boolean template annotations</h3>

    <p>{@linkplain alloy.bool.BoolTemplateInstance Annotations} can be attached to Boolean nodes to be
      used during the grounding-out of a Boolean DAG.
      The annotations are used to ensure that identical ground Boolean subformulas are shared rather than
      duplicated.  These annotations are determined and placed in the package {@link alloy.sharbool}.
      Here we will only describe the semantics of the annotations, and the correctness conditions on them.</p>
    
    <p>
      
      </p>

    <h3>Unsatisfiable cores</h3>

    Let's try to describe the current semantic guarantee.

    The lifted DAG represents a particular Boolean function.  Some nodes of the lifted DAG are annotated with
    {@linkplain alloy.bool.BoolTemplateInstance Boolean template annotations}.  The DAG also represents a particular
    ground DAG (before simplification).  The BoolStencil marks certain nodes of this ground DAG as
    being irrelevant.   What does it mean in terms of semantics?  From each node of the ground DAG,
    (more precisely -- node-and-children unit), a set of CNF clauses is written.  We had this notion
    of marking some edges a "phantom".  Some nodes of the ground DAG represent particular Boolean template
    instantiations.  Note that when we map back, we highlight the ground AST.  And ground DAG nodes
    that are annotated have specific semantic meaning with respect to the ground AST nodes -- even if
    we obtain them differently.  [Can argue about the benefits of having a stand-alone Boolean backend
    to which everything can be translated, and which doesn't need to know anything about Alloy language
    semantics.)

    So, rather than producing clauses directly from a ground AST node, what happens is that we produce
    semantically meaningful Boolean DAG nodes.  And the literals allocated to these semantically meaningful
    DAG nodes are precisely the literals we would allocate in the more direct scheme.  
 
    So, what would happen if we changed the node function computed by a ground AST node?
    The only part of the ground DAG that would change, is the part connecting this node
    to the children.

    So, we now have a notion of "relaxing" a node.  Given a ground Boolean DAG, we determine that
    some nodes of it may be "relaxed" without making the DAG satisfiable.  Some of these nodes
    have semantic meaning with respect to the ground AST.  I.e. the Boolean function they compute
    is meaningful in terms of the relational model.  Now, suppose all ground Boolean DAG nodes
    making up a ground AST node are relaxable.  So, we can relax the ground AST node by relaxing
    the ground DAG nodes that depend on it.
  
    Now, let's try to establish a more formal relationship between ground AST nodes and ground Boolean DAG
    nodes.  (Note that what we're marking up for the user are ground AST nodes, so he has to do a mental
    grounding-out of the AST to make sense of our annotations.  So we can talk in terms of what happens
    when we relax a _ground_ AST node that we have marked as relaxable.)  

    So, what does a Boolean instance annotation mean?  It means that that this ground Boolean DAG node
    computes a particular ground function.  E.g. it computes the presence of the first element of a 
    two-element set.  

    A separate thing: can try to show that if all ground forms of a lifted node are relaxable then
    the lifted node itself is relaxable.

    Ideally we would have a procedure to highlight just the text.  Esp. when entire lifted branches
    can be pruned.

    So, the sanity/correctness argument goes as follows.  We can only relax all ground nodes which 
    are a particular instantiation of a particular template, at once.  [Which are _identified as_
    instantiations of that template].  Semantically, relaxing them can be done by keeping a list
    of the corresponding Boolean instantiations, and marking the corresponding ground node as relaxed.
    When writing out a relaxed ground Boolean node, don't write the clauses that connect it to its children.
    Note that some relaxed ground node may be simplified away; that is fine.  Note that the ground DAG
    has the same shape as before, with some nodes marked as relaxed.  A node can only be marked as relaxed
    if its literal wasn't used in any clauses in the core.

    So, let's actually write some code to check that on re-translation, what we get is
    a superset of the core (as opposed to just something unsatisfiable).  This will give the
    greatest confidence.  I.e. for each clause of the core we want to check that it is in the
    re-translated .cnf file.  Also need to fix the ucore bugs we've had.

    Now, note that a given ground DAG node may match several Boolean templates, and a literal and its
    negation may match different Boolean templates (or one may match a Boolean template and the
    other not match any Boolean templates).  

    <hr>
    <address><a href="mailto:ilya_shl@mit.edu"></a></address>
<!-- Created: Sat Jun 15 21:13:56 Eastern Daylight Time 2002 -->
<!-- hhmts start -->
Last modified: Wed Dec 03 12:36:16 Eastern Standard Time 2003
<!-- hhmts end -->
  </body>
</html>
